the_es:ES, e:E. before(e)  E List 

latex

Definitions	t  T, x:A. B(x), P  Q, E, , AB, False, A, True, T, (e <loc e'), Prop, x:A. B(x), SWellFounded(R(x;y)), ES, ij, pred(e), before(e), as @ bs, b, b, , first(e), P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, append wf, es-pred wf, es-pred-locl, ge wf, nat properties, event system wf, es-locl-swellfnd, es-locl wf, le wf, nat wf, es-E wf